\begin{tabbing}
(\%S\% 
\\[0ex]$\backslash$p\=. \+
\\[0ex]let UA = get\_term\_arg `UA` p 
\\[0ex]in let A = get\_term\_arg `A` p 
\\[0ex]
\\[0ex]in let e = get\_term\_arg `e` p 
\\[0ex]in let x = get\_term\_arg `x` p 
\\[0ex]i\=n \+
\\[0ex]As\=sertL \+
\\[0ex]
\\[0ex][mk\_member\_term UA A 
\\[0ex];mk\_member\_term A e 
\\[0ex];mk\_all\_term (dv x) A (
\-\-\-\\[0ex]mk\_\=me\=mber\_term \=\+\+\+
\\[0ex]UA (mk\_equal\_term A e x)) 
\-\\[0ex]] 
\-\\[0ex]p)
\-
\end{tabbing}